\begin{tabbing}
R{-}FeasibleWitness\=\{i:l\}\+
\\[0ex]($R$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ Rnone() = Rnone() $\in$ es\_realizer\{i:l\}
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.${\it rec}_{1}$ \& ${\it rec}_{2}$
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ ${\it cl}$(${\it loc}$,$<$1, $x$$>$) = Rinit(${\it loc}$;$T$;$x$;$v$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& ${\it sv}$($x$) = $<$$T$, $v$$>$ $\in$ ($A$:Type\{i\} $\times$ ($A$ + ($\mathbb{Q}\rightarrow$$A$)))
\\[0ex]\& ${\it dis}$(${\it loc}$,$x$) = isl($v$) $\in$ $\mathbb{B}$
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$2, $x$$>$) = Rframe(${\it loc}$;$T$;$x$;$L$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& ((${\it sv}$($x$)).1) = $T$ $\in$ Type\{i\}
\\[0ex]\& ${\it fr}$(${\it loc}$,$x$) = $L$ $\in$ (Knd List)
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ \=${\it cl}$(source(${\it lnk}$),$<$3, ${\it lnk}$, ${\it tag}$$>$)\+
\\[0ex]=
\\[0ex]Rsframe(${\it lnk}$;${\it tag}$;$L$)
\\[0ex]$\in$ es\_realizer\{i:l\}
\-\\[0ex]\& ${\it sfr}$(${\it lnk}$,${\it tag}$) = $L$ $\in$ (Knd List)
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ \=${\it cl}$(${\it loc}$,$<$4, ${\it knd}$, $x$$>$)\+
\\[0ex]=
\\[0ex]Reffect(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$)
\\[0ex]$\in$ es\_realizer\{i:l\}
\-\\[0ex]\& isl($f$) = isl((${\it sv}$($x$)).2) $\in$ $\mathbb{B}$
\\[0ex]\& IdIdDeq$\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$ $\in$ Type\{i\} \& ${\it av}$(${\it knd}$) = $T$ $\in$ Type\{i\}
\\[0ex]\& (($\uparrow$isrcv(${\it knd}$)) $\Rightarrow$ (${\it loc}$ = destination(lnk(${\it knd}$)) $\in$ Id))
\\[0ex]\& (${\it knd}$ $\in$ ${\it fr}$(${\it loc}$,$x$) $\in$ Knd)
\\[0ex]\& l\_all(fpf{-}domain(${\it ds}$);Id;$z$.(${\it knd}$ $\in$ ${\it rfr}$(${\it loc}$,$z$) $\in$ Knd))
\\[0ex]\& ${\it dis}$(${\it loc}$,$x$) = isl($f$) $\in$ $\mathbb{B}$
\\[0ex]\& (($\uparrow$can{-}apply(${\it afr}$(${\it loc}$);${\it knd}$)) $\Rightarrow$ ($x$ $\in$ do{-}apply(${\it afr}$(${\it loc}$);${\it knd}$) $\in$ Id))
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ \=${\it cl}$(source($l$),$<$5, ${\it knd}$, $l$$>$)\+
\\[0ex]=
\\[0ex]Rsends(${\it ds}$;${\it knd}$;$T$;$l$;${\it dt}$;$g$)
\\[0ex]$\in$ es\_realizer\{i:l\}
\-\\[0ex]\& (\=($\uparrow$isrcv(${\it knd}$))\+
\\[0ex]$\Rightarrow$ \=((($\uparrow$lnk(${\it knd}$) = $l$) $\Rightarrow$ ($T$ = fpf{-}cap(${\it dt}$;IdDeq;tag(${\it knd}$);Void) $\in$ Type\{i\}))\+
\\[0ex]\& destination(lnk(${\it knd}$)) = source($l$) $\in$ Id))
\-\-\\[0ex]\& IdIdDeq$\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$ $\in$ Type\{i\}
\\[0ex]\& ${\it av}$(${\it knd}$) = $T$ $\in$ Type\{i\}
\\[0ex]\& KndKindDeq$\forall$$k$$\in$dom(lnk{-}decl($l$;${\it dt}$)). $A$=lnk{-}decl($l$;${\it dt}$)($k$) $\Rightarrow$  ${\it av}$($k$) = $A$ $\in$ Type\{i\}
\\[0ex]\& normal{-}ds\=\{i:l\}\+
\\[0ex](${\it dt}$)
\-\\[0ex]\& l\_all(map($\lambda$$p$.$p$.1;$g$);Id;${\it tg}$.(${\it knd}$ $\in$ ${\it sfr}$($l$,${\it tg}$) $\in$ Knd))
\\[0ex]\& l\_all(fpf{-}domain(${\it ds}$);Id;$z$.(${\it knd}$ $\in$ ${\it rfr}$(source($l$),$z$) $\in$ Knd))
\\[0ex]\& (($\uparrow$can{-}apply(${\it bfr}$(source($l$));${\it knd}$)) $\Rightarrow$ ($l$ $\in$ do{-}apply(${\it bfr}$(source($l$));${\it knd}$) $\in$ IdLnk))
\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$p$,$P$)=$>$ ${\it cl}$(${\it loc}$,$<$6, $a$$>$) = Rpre(${\it loc}$;${\it ds}$;$a$;$p$;$P$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& IdIdDeq$\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$ $\in$ Type\{i\}
\\[0ex]\& ${\it av}$(locl($a$)) = p{-}outcome($p$) $\in$ Type\{i\}
\\[0ex]\& l\_all(fpf{-}domain(${\it ds}$);Id;$z$.(locl($a$) $\in$ ${\it rfr}$(${\it loc}$,$z$) $\in$ Knd))
\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$7, $k$$>$) = Raframe(${\it loc}$;$k$;$L$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& ${\it afr}$(${\it loc}$,$k$) = (inl $L$ ) $\in$ ((Id List) + Top)
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$8, $k$$>$) = Rbframe(${\it loc}$;$k$;$L$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& ${\it bfr}$(${\it loc}$,$k$) = (inl $L$ ) $\in$ ((IdLnk List) + Top)
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$9, $x$$>$) = Rrframe(${\it loc}$;$x$;$L$) $\in$ es\_realizer\{i:l\}
\\[0ex]\& ${\it rfr}$(${\it loc}$,$x$) = $L$ $\in$ (Knd List)
\-
\end{tabbing}